Nuprl Lemma : sign_wf
11,40
postcript
pdf
x
:
. sign(
x
)
latex
Definitions
sign(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
le
int
wf
,
ifthenelse
wf
origin
x:
. sign(x) 
x:. sign(x) Tx:A. B(x)